Inference at * 1 1 3 
Iof proof for Lemma add functionality wrt le:



1. i2 : 
2. j2 : 
3. i2  j2
4. i1 : 
5. 0 < i1
6. j1:. ((i1 - 1)  j1)  (((i1 - 1)+i2)  (j1+j2))
7. j1 : 
8. i1  j1
  (i1+i2)  (j1+j2) 

latex

 by (RA ((DTerm j1 - 1 6) 
CollapseTHENM (D (-1)))) 

latex

C.

Definitions

False, A, t  T, P  Q, A  B, x:A. B(x)